$\forall$$T$:Type, ${\it pl}$, ${\it tm}$:($T$$\rightarrow$$T$$\rightarrow$$T$).
\\[0ex]Comm($T$;${\it tm}$)
\\[0ex]$\Rightarrow$ ($\forall$$a$, $x$, $y$:$T$. ($a$ ${\it tm}$ ($x$ ${\it pl}$ $y$)) = (($a$ ${\it tm}$ $x$) ${\it pl}$ ($a$ ${\it tm}$ $y$)) $\in$ $T$)
\\[0ex]$\Rightarrow$ BiLinear($T$;${\it pl}$;${\it tm}$)